Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		terms(N)	→ cons(recip(sqr(N)),terms(s(N)))
2:		sqr(0)	→ 0
3:		sqr(s(X))	→ s(add(sqr(X),dbl(X)))
4:		dbl(0)	→ 0
5:		dbl(s(X))	→ s(s(dbl(X)))
6:		add(0,X)	→ X
7:		add(s(X),Y)	→ s(add(X,Y))
8:		first(0,X)	→ nil
9:		first(s(X),cons(Y,Z))	→ cons(Y,first(X,Z))

There are 8 dependency pairs:


10:		TERMS(N)	→ SQR(N)
11:		TERMS(N)	→ TERMS(s(N))
12:		SQR(s(X))	→ ADD(sqr(X),dbl(X))
13:		SQR(s(X))	→ SQR(X)
14:		SQR(s(X))	→ DBL(X)
15:		DBL(s(X))	→ DBL(X)
16:		ADD(s(X),Y)	→ ADD(X,Y)
17:		FIRST(s(X),cons(Y,Z))	→ FIRST(X,Z)

The approximated dependency graph contains 5 SCCs: {16}, {15}, {17}, {13} and {11}.

Consider the SCC {16}. There are no usable rules. By taking the AF π with π(ADD) = 1 together with the lexicographic path order with empty precedence, rule 16 is strictly decreasing.

Consider the SCC {15}. There are no usable rules. By taking the AF π with π(DBL) = 1 together with the lexicographic path order with empty precedence, rule 15 is strictly decreasing.

Consider the SCC {17}. There are no usable rules. By taking the AF π with π(FIRST) = 1 together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {13}. There are no usable rules. By taking the AF π with π(SQR) = 1 together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.

Consider the SCC {11}. There are no usable rules. The constraints could not be solved.

Tyrolean Termination Tool (0.02 seconds) --- May 3, 2006